es:ES, e:E, l:IdLnk, tg:Id, T:Type, v:T.
{m:Msg| source(mlnk(m)) = source(l)  Id }  Msg(l',tg'. if l' = l  tg' = tg T else Top fi)
 sends(l;e) = [msg(l;tg;v)]  Msg(l',tg'. if l' = l  tg' = tg T else Top fi) List
 (e':E.
 (kind(e') = rcv(l,tg)  Knd & val(e') = v & sender(e') = e
 (& (e'':E. kind(e'') = rcv(l,tg)  Knd  sender(e'') = e  e'' = e')) 

latex

Definitions

ES, t  T, x:A. B(x), E, IdLnk, Id, Top, a = b, a = b, p  q, if b t else f fi, Msg(M), source(l), mlnk(m), Msg, msg(l;t;v), (Msg on l), S  T, sends(l;e), Prop, Knd, P & Q, A & B, x:A. B(x), P  Q, ||as||, AB, i  j < k, False, A, {i..j}, l[i], sender(e), lnk(e), index(e), True, T, val(e), tag(e), b, P  Q, b, , p  q, P  Q, P  Q, Unit, hd(l), i<j, ij, x. t(x), 1of(t), 2of(t), , rcv(l,tg), kind(e), isrcv(e), isrcv(k), loc(e), destination(l), lnk(k), locl(a), {T}, SQType(T), (e <loc e'), ij, valtype(e), haslink(l;m)

Lemmas

subtype rel transitivity, es-kind-rcv, es-Msg-subtype1, es-val wf, Knd wf, es-kind wf, length wf1, es-Msgl wf, es-lnk wf, es-sends wf, es-locl-antireflexive, es-locl wf, es-index wf, int seg wf, lnk wf, isrcv wf, ldst wf, es-loc wf, es-sender wf, rcv wf, isrcv-implies, pi2 wf, pi1 wf, mlnk wf, member wf, eqtt to assert, assert of band, and functionality wrt iff, eqff to assert, bnot thru band, assert of bor, or functionality wrt iff, assert-eq-lnk, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bool wf, bor wf, bnot wf, not wf, assert wf, true wf, select wf, squash wf, le wf, es-axioms, msg wf, es-Msg wf, mlnk wf2, lsrc wf, Msg wf, ifthenelse wf, band wf, eq lnk wf, eq id wf, top wf, Id wf, IdLnk wf, es-E wf, event system wf